Correctly implement δ-resolver lift for modules. - #22451

Module δ-resolvers are morally a kind of substitution, associating
a canonical name to some aliased constant. Functors and module types
are function-like w.r.t. to resolvers, insofar as the name they introduce
is bound and should be left alone. This is similar to the λ-calculus
equation (λt){σ} ≡ λ(t{σ↑}) where substitutions must be lifted when going
under a context.

Unfortunately, the resolver mechanism is not based on De Bruijn indices
but names, and the implementation was implementing the lift in a broken
way, by adding the trivial equivalence p ↦ p for some bound path p.
As is expected, this does not play well with the usual algebraic
operations one expect to apply to resolvers, leading to interesting
breakage of invariants here and there. It did not seem enough to prove
False though, just random anomalies and incompletenesses.

We fix this mess by introducing an explicit lift operation in δ-resolvers
which is handled specifically by substitution. En passant, the internals
of Mod_subst are horrendous as they rely on physical equality (!) for some
reason, resulting in interesting eisenbugs while trying to change the
implementation.

Fixes rocq-prover#22426: Self-equivalence within δ-resolvers not stable by aliasing.